Skip to content

[ refactor ] Redefine Relation.Binary.Definitions.Adjoint, plus knock-on Function.Consequences#2599

Open
jamesmckinna wants to merge 15 commits into
agda:masterfrom
jamesmckinna:issue2581
Open

[ refactor ] Redefine Relation.Binary.Definitions.Adjoint, plus knock-on Function.Consequences#2599
jamesmckinna wants to merge 15 commits into
agda:masterfrom
jamesmckinna:issue2581

Conversation

@jamesmckinna

@jamesmckinna jamesmckinna commented Feb 19, 2025

Copy link
Copy Markdown
Collaborator

Fixes #2581 .

@jamesmckinna jamesmckinna added this to the v3.0 milestone Feb 19, 2025
@jamesmckinna jamesmckinna marked this pull request as draft February 19, 2025 19:24
@jamesmckinna jamesmckinna marked this pull request as ready for review February 20, 2025 07:38
@jamesmckinna

Copy link
Copy Markdown
Collaborator Author

I'll return to the merge conflicts after v2.3, given that this is a breaking change.

Comment thread src/Function/Consequences/Setoid.agda
@jamesmckinna

Copy link
Copy Markdown
Collaborator Author

Given how many of these breaking changes arise from the analysis developed in specific issues, I've evolved my approach to the CHANGELOG by explicitly linking to those issues under each item. Feedback welcome on whether this is desirable or not!

At present, two existing such items are badly formatted, so at some point, we should fix those up, but I won't try to as part of this PR (though at some level, to me at least, it would 'make sense' to do so, to be consistent with the entry added here... ;-))

@JacquesCarette JacquesCarette left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It is easy to remove these links later if we wish, way harder to add them post facto. So I'm all for having them in!

@jamesmckinna

Copy link
Copy Markdown
Collaborator Author

Just fixed a typo, and with it the chance to look over everything once again. I'd like to merge this, but at that point, we basically will have duplicate families Half*Adjoint and Inverse*, so downstream we should try to reconcile everything under a single sensible naming scheme...

@JacquesCarette

Copy link
Copy Markdown
Collaborator

I don't understand your comment about duplication? Yes, these are equivalent notions, but with rather different UX, so having them both is definitely a plus.

@jamesmckinna

Copy link
Copy Markdown
Collaborator Author

Thanks @JacquesCarette re:duplication. Will not fiddle any further.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

[ refactor ] Reconcile Relation.Binary.Definitions.Adjoint and Function.Definitions.Inverse*

2 participants